Left Termination of the query pattern e_in_2(g, a) w.r.t. the given Prolog program could successfully be proven:



↳ Prolog
  ↳ PrologToPiTRSProof

Clauses:

e(L, T) :- t(L, T).
e(L, T) :- ','(t(L, .(plus, C)), e(C, T)).
t(L, T) :- n(L, T).
t(L, T) :- ','(n(L, .(star, C)), t(C, T)).
n(.(L, T), T) :- z(L).
n(.(lbrace, A), B) :- e(A, .(rbrace, B)).
z(a).
z(b).
z(c).

Queries:

e(g,a).

We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
e_in: (b,f)
t_in: (b,f)
n_in: (b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

e_in_ga(L, T) → U1_ga(L, T, t_in_ga(L, T))
t_in_ga(L, T) → U4_ga(L, T, n_in_ga(L, T))
n_in_ga(.(L, T), T) → U7_ga(L, T, z_in_g(L))
z_in_g(a) → z_out_g(a)
z_in_g(b) → z_out_g(b)
z_in_g(c) → z_out_g(c)
U7_ga(L, T, z_out_g(L)) → n_out_ga(.(L, T), T)
n_in_ga(.(lbrace, A), B) → U8_ga(A, B, e_in_ga(A, .(rbrace, B)))
e_in_ga(L, T) → U2_ga(L, T, t_in_ga(L, .(plus, C)))
t_in_ga(L, T) → U5_ga(L, T, n_in_ga(L, .(star, C)))
U5_ga(L, T, n_out_ga(L, .(star, C))) → U6_ga(L, T, t_in_ga(C, T))
U6_ga(L, T, t_out_ga(C, T)) → t_out_ga(L, T)
U2_ga(L, T, t_out_ga(L, .(plus, C))) → U3_ga(L, T, e_in_ga(C, T))
U3_ga(L, T, e_out_ga(C, T)) → e_out_ga(L, T)
U8_ga(A, B, e_out_ga(A, .(rbrace, B))) → n_out_ga(.(lbrace, A), B)
U4_ga(L, T, n_out_ga(L, T)) → t_out_ga(L, T)
U1_ga(L, T, t_out_ga(L, T)) → e_out_ga(L, T)

The argument filtering Pi contains the following mapping:
e_in_ga(x1, x2)  =  e_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
t_in_ga(x1, x2)  =  t_in_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
n_in_ga(x1, x2)  =  n_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x2, x3)
z_in_g(x1)  =  z_in_g(x1)
a  =  a
z_out_g(x1)  =  z_out_g
b  =  b
c  =  c
n_out_ga(x1, x2)  =  n_out_ga(x2)
lbrace  =  lbrace
U8_ga(x1, x2, x3)  =  U8_ga(x3)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
star  =  star
U6_ga(x1, x2, x3)  =  U6_ga(x3)
t_out_ga(x1, x2)  =  t_out_ga(x2)
plus  =  plus
U3_ga(x1, x2, x3)  =  U3_ga(x3)
e_out_ga(x1, x2)  =  e_out_ga(x2)
rbrace  =  rbrace

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

e_in_ga(L, T) → U1_ga(L, T, t_in_ga(L, T))
t_in_ga(L, T) → U4_ga(L, T, n_in_ga(L, T))
n_in_ga(.(L, T), T) → U7_ga(L, T, z_in_g(L))
z_in_g(a) → z_out_g(a)
z_in_g(b) → z_out_g(b)
z_in_g(c) → z_out_g(c)
U7_ga(L, T, z_out_g(L)) → n_out_ga(.(L, T), T)
n_in_ga(.(lbrace, A), B) → U8_ga(A, B, e_in_ga(A, .(rbrace, B)))
e_in_ga(L, T) → U2_ga(L, T, t_in_ga(L, .(plus, C)))
t_in_ga(L, T) → U5_ga(L, T, n_in_ga(L, .(star, C)))
U5_ga(L, T, n_out_ga(L, .(star, C))) → U6_ga(L, T, t_in_ga(C, T))
U6_ga(L, T, t_out_ga(C, T)) → t_out_ga(L, T)
U2_ga(L, T, t_out_ga(L, .(plus, C))) → U3_ga(L, T, e_in_ga(C, T))
U3_ga(L, T, e_out_ga(C, T)) → e_out_ga(L, T)
U8_ga(A, B, e_out_ga(A, .(rbrace, B))) → n_out_ga(.(lbrace, A), B)
U4_ga(L, T, n_out_ga(L, T)) → t_out_ga(L, T)
U1_ga(L, T, t_out_ga(L, T)) → e_out_ga(L, T)

The argument filtering Pi contains the following mapping:
e_in_ga(x1, x2)  =  e_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
t_in_ga(x1, x2)  =  t_in_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
n_in_ga(x1, x2)  =  n_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x2, x3)
z_in_g(x1)  =  z_in_g(x1)
a  =  a
z_out_g(x1)  =  z_out_g
b  =  b
c  =  c
n_out_ga(x1, x2)  =  n_out_ga(x2)
lbrace  =  lbrace
U8_ga(x1, x2, x3)  =  U8_ga(x3)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
star  =  star
U6_ga(x1, x2, x3)  =  U6_ga(x3)
t_out_ga(x1, x2)  =  t_out_ga(x2)
plus  =  plus
U3_ga(x1, x2, x3)  =  U3_ga(x3)
e_out_ga(x1, x2)  =  e_out_ga(x2)
rbrace  =  rbrace


Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

E_IN_GA(L, T) → U1_GA(L, T, t_in_ga(L, T))
E_IN_GA(L, T) → T_IN_GA(L, T)
T_IN_GA(L, T) → U4_GA(L, T, n_in_ga(L, T))
T_IN_GA(L, T) → N_IN_GA(L, T)
N_IN_GA(.(L, T), T) → U7_GA(L, T, z_in_g(L))
N_IN_GA(.(L, T), T) → Z_IN_G(L)
N_IN_GA(.(lbrace, A), B) → U8_GA(A, B, e_in_ga(A, .(rbrace, B)))
N_IN_GA(.(lbrace, A), B) → E_IN_GA(A, .(rbrace, B))
E_IN_GA(L, T) → U2_GA(L, T, t_in_ga(L, .(plus, C)))
E_IN_GA(L, T) → T_IN_GA(L, .(plus, C))
T_IN_GA(L, T) → U5_GA(L, T, n_in_ga(L, .(star, C)))
T_IN_GA(L, T) → N_IN_GA(L, .(star, C))
U5_GA(L, T, n_out_ga(L, .(star, C))) → U6_GA(L, T, t_in_ga(C, T))
U5_GA(L, T, n_out_ga(L, .(star, C))) → T_IN_GA(C, T)
U2_GA(L, T, t_out_ga(L, .(plus, C))) → U3_GA(L, T, e_in_ga(C, T))
U2_GA(L, T, t_out_ga(L, .(plus, C))) → E_IN_GA(C, T)

The TRS R consists of the following rules:

e_in_ga(L, T) → U1_ga(L, T, t_in_ga(L, T))
t_in_ga(L, T) → U4_ga(L, T, n_in_ga(L, T))
n_in_ga(.(L, T), T) → U7_ga(L, T, z_in_g(L))
z_in_g(a) → z_out_g(a)
z_in_g(b) → z_out_g(b)
z_in_g(c) → z_out_g(c)
U7_ga(L, T, z_out_g(L)) → n_out_ga(.(L, T), T)
n_in_ga(.(lbrace, A), B) → U8_ga(A, B, e_in_ga(A, .(rbrace, B)))
e_in_ga(L, T) → U2_ga(L, T, t_in_ga(L, .(plus, C)))
t_in_ga(L, T) → U5_ga(L, T, n_in_ga(L, .(star, C)))
U5_ga(L, T, n_out_ga(L, .(star, C))) → U6_ga(L, T, t_in_ga(C, T))
U6_ga(L, T, t_out_ga(C, T)) → t_out_ga(L, T)
U2_ga(L, T, t_out_ga(L, .(plus, C))) → U3_ga(L, T, e_in_ga(C, T))
U3_ga(L, T, e_out_ga(C, T)) → e_out_ga(L, T)
U8_ga(A, B, e_out_ga(A, .(rbrace, B))) → n_out_ga(.(lbrace, A), B)
U4_ga(L, T, n_out_ga(L, T)) → t_out_ga(L, T)
U1_ga(L, T, t_out_ga(L, T)) → e_out_ga(L, T)

The argument filtering Pi contains the following mapping:
e_in_ga(x1, x2)  =  e_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
t_in_ga(x1, x2)  =  t_in_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
n_in_ga(x1, x2)  =  n_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x2, x3)
z_in_g(x1)  =  z_in_g(x1)
a  =  a
z_out_g(x1)  =  z_out_g
b  =  b
c  =  c
n_out_ga(x1, x2)  =  n_out_ga(x2)
lbrace  =  lbrace
U8_ga(x1, x2, x3)  =  U8_ga(x3)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
star  =  star
U6_ga(x1, x2, x3)  =  U6_ga(x3)
t_out_ga(x1, x2)  =  t_out_ga(x2)
plus  =  plus
U3_ga(x1, x2, x3)  =  U3_ga(x3)
e_out_ga(x1, x2)  =  e_out_ga(x2)
rbrace  =  rbrace
U6_GA(x1, x2, x3)  =  U6_GA(x3)
N_IN_GA(x1, x2)  =  N_IN_GA(x1)
U5_GA(x1, x2, x3)  =  U5_GA(x3)
E_IN_GA(x1, x2)  =  E_IN_GA(x1)
T_IN_GA(x1, x2)  =  T_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x3)
U3_GA(x1, x2, x3)  =  U3_GA(x3)
Z_IN_G(x1)  =  Z_IN_G(x1)
U7_GA(x1, x2, x3)  =  U7_GA(x2, x3)
U2_GA(x1, x2, x3)  =  U2_GA(x3)
U1_GA(x1, x2, x3)  =  U1_GA(x3)
U8_GA(x1, x2, x3)  =  U8_GA(x3)

We have to consider all (P,R,Pi)-chains

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

E_IN_GA(L, T) → U1_GA(L, T, t_in_ga(L, T))
E_IN_GA(L, T) → T_IN_GA(L, T)
T_IN_GA(L, T) → U4_GA(L, T, n_in_ga(L, T))
T_IN_GA(L, T) → N_IN_GA(L, T)
N_IN_GA(.(L, T), T) → U7_GA(L, T, z_in_g(L))
N_IN_GA(.(L, T), T) → Z_IN_G(L)
N_IN_GA(.(lbrace, A), B) → U8_GA(A, B, e_in_ga(A, .(rbrace, B)))
N_IN_GA(.(lbrace, A), B) → E_IN_GA(A, .(rbrace, B))
E_IN_GA(L, T) → U2_GA(L, T, t_in_ga(L, .(plus, C)))
E_IN_GA(L, T) → T_IN_GA(L, .(plus, C))
T_IN_GA(L, T) → U5_GA(L, T, n_in_ga(L, .(star, C)))
T_IN_GA(L, T) → N_IN_GA(L, .(star, C))
U5_GA(L, T, n_out_ga(L, .(star, C))) → U6_GA(L, T, t_in_ga(C, T))
U5_GA(L, T, n_out_ga(L, .(star, C))) → T_IN_GA(C, T)
U2_GA(L, T, t_out_ga(L, .(plus, C))) → U3_GA(L, T, e_in_ga(C, T))
U2_GA(L, T, t_out_ga(L, .(plus, C))) → E_IN_GA(C, T)

The TRS R consists of the following rules:

e_in_ga(L, T) → U1_ga(L, T, t_in_ga(L, T))
t_in_ga(L, T) → U4_ga(L, T, n_in_ga(L, T))
n_in_ga(.(L, T), T) → U7_ga(L, T, z_in_g(L))
z_in_g(a) → z_out_g(a)
z_in_g(b) → z_out_g(b)
z_in_g(c) → z_out_g(c)
U7_ga(L, T, z_out_g(L)) → n_out_ga(.(L, T), T)
n_in_ga(.(lbrace, A), B) → U8_ga(A, B, e_in_ga(A, .(rbrace, B)))
e_in_ga(L, T) → U2_ga(L, T, t_in_ga(L, .(plus, C)))
t_in_ga(L, T) → U5_ga(L, T, n_in_ga(L, .(star, C)))
U5_ga(L, T, n_out_ga(L, .(star, C))) → U6_ga(L, T, t_in_ga(C, T))
U6_ga(L, T, t_out_ga(C, T)) → t_out_ga(L, T)
U2_ga(L, T, t_out_ga(L, .(plus, C))) → U3_ga(L, T, e_in_ga(C, T))
U3_ga(L, T, e_out_ga(C, T)) → e_out_ga(L, T)
U8_ga(A, B, e_out_ga(A, .(rbrace, B))) → n_out_ga(.(lbrace, A), B)
U4_ga(L, T, n_out_ga(L, T)) → t_out_ga(L, T)
U1_ga(L, T, t_out_ga(L, T)) → e_out_ga(L, T)

The argument filtering Pi contains the following mapping:
e_in_ga(x1, x2)  =  e_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
t_in_ga(x1, x2)  =  t_in_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
n_in_ga(x1, x2)  =  n_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x2, x3)
z_in_g(x1)  =  z_in_g(x1)
a  =  a
z_out_g(x1)  =  z_out_g
b  =  b
c  =  c
n_out_ga(x1, x2)  =  n_out_ga(x2)
lbrace  =  lbrace
U8_ga(x1, x2, x3)  =  U8_ga(x3)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
star  =  star
U6_ga(x1, x2, x3)  =  U6_ga(x3)
t_out_ga(x1, x2)  =  t_out_ga(x2)
plus  =  plus
U3_ga(x1, x2, x3)  =  U3_ga(x3)
e_out_ga(x1, x2)  =  e_out_ga(x2)
rbrace  =  rbrace
U6_GA(x1, x2, x3)  =  U6_GA(x3)
N_IN_GA(x1, x2)  =  N_IN_GA(x1)
U5_GA(x1, x2, x3)  =  U5_GA(x3)
E_IN_GA(x1, x2)  =  E_IN_GA(x1)
T_IN_GA(x1, x2)  =  T_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x3)
U3_GA(x1, x2, x3)  =  U3_GA(x3)
Z_IN_G(x1)  =  Z_IN_G(x1)
U7_GA(x1, x2, x3)  =  U7_GA(x2, x3)
U2_GA(x1, x2, x3)  =  U2_GA(x3)
U1_GA(x1, x2, x3)  =  U1_GA(x3)
U8_GA(x1, x2, x3)  =  U8_GA(x3)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 1 SCC with 7 less nodes.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

T_IN_GA(L, T) → U5_GA(L, T, n_in_ga(L, .(star, C)))
E_IN_GA(L, T) → T_IN_GA(L, T)
E_IN_GA(L, T) → T_IN_GA(L, .(plus, C))
E_IN_GA(L, T) → U2_GA(L, T, t_in_ga(L, .(plus, C)))
U2_GA(L, T, t_out_ga(L, .(plus, C))) → E_IN_GA(C, T)
T_IN_GA(L, T) → N_IN_GA(L, T)
T_IN_GA(L, T) → N_IN_GA(L, .(star, C))
U5_GA(L, T, n_out_ga(L, .(star, C))) → T_IN_GA(C, T)
N_IN_GA(.(lbrace, A), B) → E_IN_GA(A, .(rbrace, B))

The TRS R consists of the following rules:

e_in_ga(L, T) → U1_ga(L, T, t_in_ga(L, T))
t_in_ga(L, T) → U4_ga(L, T, n_in_ga(L, T))
n_in_ga(.(L, T), T) → U7_ga(L, T, z_in_g(L))
z_in_g(a) → z_out_g(a)
z_in_g(b) → z_out_g(b)
z_in_g(c) → z_out_g(c)
U7_ga(L, T, z_out_g(L)) → n_out_ga(.(L, T), T)
n_in_ga(.(lbrace, A), B) → U8_ga(A, B, e_in_ga(A, .(rbrace, B)))
e_in_ga(L, T) → U2_ga(L, T, t_in_ga(L, .(plus, C)))
t_in_ga(L, T) → U5_ga(L, T, n_in_ga(L, .(star, C)))
U5_ga(L, T, n_out_ga(L, .(star, C))) → U6_ga(L, T, t_in_ga(C, T))
U6_ga(L, T, t_out_ga(C, T)) → t_out_ga(L, T)
U2_ga(L, T, t_out_ga(L, .(plus, C))) → U3_ga(L, T, e_in_ga(C, T))
U3_ga(L, T, e_out_ga(C, T)) → e_out_ga(L, T)
U8_ga(A, B, e_out_ga(A, .(rbrace, B))) → n_out_ga(.(lbrace, A), B)
U4_ga(L, T, n_out_ga(L, T)) → t_out_ga(L, T)
U1_ga(L, T, t_out_ga(L, T)) → e_out_ga(L, T)

The argument filtering Pi contains the following mapping:
e_in_ga(x1, x2)  =  e_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
t_in_ga(x1, x2)  =  t_in_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
n_in_ga(x1, x2)  =  n_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x2, x3)
z_in_g(x1)  =  z_in_g(x1)
a  =  a
z_out_g(x1)  =  z_out_g
b  =  b
c  =  c
n_out_ga(x1, x2)  =  n_out_ga(x2)
lbrace  =  lbrace
U8_ga(x1, x2, x3)  =  U8_ga(x3)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
star  =  star
U6_ga(x1, x2, x3)  =  U6_ga(x3)
t_out_ga(x1, x2)  =  t_out_ga(x2)
plus  =  plus
U3_ga(x1, x2, x3)  =  U3_ga(x3)
e_out_ga(x1, x2)  =  e_out_ga(x2)
rbrace  =  rbrace
N_IN_GA(x1, x2)  =  N_IN_GA(x1)
U5_GA(x1, x2, x3)  =  U5_GA(x3)
E_IN_GA(x1, x2)  =  E_IN_GA(x1)
T_IN_GA(x1, x2)  =  T_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x3)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ PiDPToQDPProof
                ↳ QDP
                  ↳ UsableRulesReductionPairsProof

Q DP problem:
The TRS P consists of the following rules:

U2_GA(t_out_ga(.(plus, C))) → E_IN_GA(C)
T_IN_GA(L) → N_IN_GA(L)
E_IN_GA(L) → T_IN_GA(L)
E_IN_GA(L) → U2_GA(t_in_ga(L))
N_IN_GA(.(lbrace, A)) → E_IN_GA(A)
U5_GA(n_out_ga(.(star, C))) → T_IN_GA(C)
T_IN_GA(L) → U5_GA(n_in_ga(L))

The TRS R consists of the following rules:

e_in_ga(L) → U1_ga(t_in_ga(L))
t_in_ga(L) → U4_ga(n_in_ga(L))
n_in_ga(.(L, T)) → U7_ga(T, z_in_g(L))
z_in_g(a) → z_out_g
z_in_g(b) → z_out_g
z_in_g(c) → z_out_g
U7_ga(T, z_out_g) → n_out_ga(T)
n_in_ga(.(lbrace, A)) → U8_ga(e_in_ga(A))
e_in_ga(L) → U2_ga(t_in_ga(L))
t_in_ga(L) → U5_ga(n_in_ga(L))
U5_ga(n_out_ga(.(star, C))) → U6_ga(t_in_ga(C))
U6_ga(t_out_ga(T)) → t_out_ga(T)
U2_ga(t_out_ga(.(plus, C))) → U3_ga(e_in_ga(C))
U3_ga(e_out_ga(T)) → e_out_ga(T)
U8_ga(e_out_ga(.(rbrace, B))) → n_out_ga(B)
U4_ga(n_out_ga(T)) → t_out_ga(T)
U1_ga(t_out_ga(T)) → e_out_ga(T)

The set Q consists of the following terms:

e_in_ga(x0)
t_in_ga(x0)
n_in_ga(x0)
z_in_g(x0)
U7_ga(x0, x1)
U5_ga(x0)
U6_ga(x0)
U2_ga(x0)
U3_ga(x0)
U8_ga(x0)
U4_ga(x0)
U1_ga(x0)

We have to consider all (P,Q,R)-chains.
By using the usable rules with reduction pair processor [15] with a polynomial ordering [25], all dependency pairs and the corresponding usable rules [17] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

U2_GA(t_out_ga(.(plus, C))) → E_IN_GA(C)
E_IN_GA(L) → T_IN_GA(L)
E_IN_GA(L) → U2_GA(t_in_ga(L))
N_IN_GA(.(lbrace, A)) → E_IN_GA(A)
U5_GA(n_out_ga(.(star, C))) → T_IN_GA(C)
The following rules are removed from R:

n_in_ga(.(L, T)) → U7_ga(T, z_in_g(L))
n_in_ga(.(lbrace, A)) → U8_ga(e_in_ga(A))
U5_ga(n_out_ga(.(star, C))) → U6_ga(t_in_ga(C))
U6_ga(t_out_ga(T)) → t_out_ga(T)
U8_ga(e_out_ga(.(rbrace, B))) → n_out_ga(B)
U2_ga(t_out_ga(.(plus, C))) → U3_ga(e_in_ga(C))
U3_ga(e_out_ga(T)) → e_out_ga(T)
z_in_g(a) → z_out_g
z_in_g(b) → z_out_g
z_in_g(c) → z_out_g
Used ordering: POLO with Polynomial interpretation [25]:

POL(.(x1, x2)) = 2 + x1 + 2·x2   
POL(E_IN_GA(x1)) = 2 + 2·x1   
POL(N_IN_GA(x1)) = x1   
POL(T_IN_GA(x1)) = 2·x1   
POL(U1_ga(x1)) = x1   
POL(U2_GA(x1)) = x1   
POL(U2_ga(x1)) = x1   
POL(U3_ga(x1)) = 1 + 2·x1   
POL(U4_ga(x1)) = x1   
POL(U5_GA(x1)) = x1   
POL(U5_ga(x1)) = x1   
POL(U6_ga(x1)) = 2 + x1   
POL(U7_ga(x1, x2)) = x1 + x2   
POL(U8_ga(x1)) = 2 + x1   
POL(a) = 2   
POL(b) = 1   
POL(c) = 2   
POL(e_in_ga(x1)) = x1   
POL(e_out_ga(x1)) = 2 + x1   
POL(lbrace) = 0   
POL(n_in_ga(x1)) = x1   
POL(n_out_ga(x1)) = 2 + x1   
POL(plus) = 1   
POL(rbrace) = 1   
POL(star) = 1   
POL(t_in_ga(x1)) = x1   
POL(t_out_ga(x1)) = 2 + x1   
POL(z_in_g(x1)) = 1 + x1   
POL(z_out_g) = 2   



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ PiDPToQDPProof
                ↳ QDP
                  ↳ UsableRulesReductionPairsProof
                    ↳ QDP
                      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

T_IN_GA(L) → N_IN_GA(L)
T_IN_GA(L) → U5_GA(n_in_ga(L))

The TRS R consists of the following rules:

t_in_ga(L) → U4_ga(n_in_ga(L))
t_in_ga(L) → U5_ga(n_in_ga(L))
e_in_ga(L) → U1_ga(t_in_ga(L))
e_in_ga(L) → U2_ga(t_in_ga(L))
U1_ga(t_out_ga(T)) → e_out_ga(T)
U7_ga(T, z_out_g) → n_out_ga(T)
U4_ga(n_out_ga(T)) → t_out_ga(T)

The set Q consists of the following terms:

e_in_ga(x0)
t_in_ga(x0)
n_in_ga(x0)
z_in_g(x0)
U7_ga(x0, x1)
U5_ga(x0)
U6_ga(x0)
U2_ga(x0)
U3_ga(x0)
U8_ga(x0)
U4_ga(x0)
U1_ga(x0)

We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 2 less nodes.